package sat;

import java.util.HashMap;
import java.util.Iterator;
import sat.convenience.Solution;

/**
 * Zestaw narzędzi wspierających przeprowadzenie symulowanego wyżarzania.
 * @author bawey
 */
public class SasatToolkit {
    
    /**
     * Funkcja oblicza potencjalne poprawy jakości rozwiązania wynikające
     * z zanegowania każdego pojedynczego przypisania (osobno)
     * @param solution - obecne podstawienia
     * @param formula - formuła logiczna poddana rozważaniom
     * @return HashMap<ZanegowanyLiterał,ZyskZZanegowania>
     */
    public static HashMap<String, Float> calculatePotentialGains(FormulaCNF formula, Solution solution) {
        HashMap<String, Float> result = new HashMap<String, Float>();
        for (Iterator it = solution.keySet().iterator(); it.hasNext();) {
            String key = (String) it.next();
            result.put(key, new Float(calculatePotentialGain(formula, solution, key)));
        }
        return result;
    }

    /**
     * Funkcja oblicza zysk na jakości rozwiązania uzyskany poprzez zanegowanie
     * wartości przypisanej danemu symbolowi
     * @param formula formuła logiczna
     * @param solution oryginalne rozwiązanie
     * @param key rozpatrywany symbol
     * @return 
     */
    public static float calculatePotentialGain(FormulaCNF formula, Solution solution, String key) {
        solution.put(key, solution.get(key).booleanValue() ? Boolean.FALSE : Boolean.TRUE);
        float flippedQuality = formula.getWeighedTrueClausesPercentage(solution);
        //flip back
        solution.put(key, solution.get(key).booleanValue() ? Boolean.FALSE : Boolean.TRUE);
        float initialQuality = formula.getWeighedTrueClausesPercentage(solution);
        return flippedQuality - initialQuality;
    }
}
